Termination w.r.t. Q proof of TRS/AProVELiveness6.3.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

TOP(rec(up(x))) → REC(x)
CHECK(no(x)) → CHECK(x)
REC(bot) → SENT(bot)
REC(rec(x)) → SENT(rec(x))
TOP(sent(up(x))) → CHECK(rec(x))
CHECK(rec(x)) → CHECK(x)
REC(up(x)) → REC(x)
TOP(no(up(x))) → REC(x)
TOP(sent(up(x))) → TOP(check(rec(x)))
REC(no(x)) → SENT(rec(x))
CHECK(sent(x)) → SENT(check(x))
CHECK(rec(x)) → REC(check(x))
TOP(no(up(x))) → CHECK(rec(x))
CHECK(no(x)) → NO(check(x))
REC(sent(x)) → SENT(rec(x))
CHECK(up(x)) → CHECK(x)
TOP(sent(up(x))) → REC(x)
TOP(rec(up(x))) → CHECK(rec(x))
TOP(no(up(x))) → TOP(check(rec(x)))
REC(no(x)) → REC(x)
NO(up(x)) → NO(x)
SENT(up(x)) → SENT(x)
TOP(rec(up(x))) → TOP(check(rec(x)))
REC(sent(x)) → REC(x)
CHECK(sent(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

TOP(rec(up(x))) → REC(x)
CHECK(no(x)) → CHECK(x)
REC(bot) → SENT(bot)
REC(rec(x)) → SENT(rec(x))
TOP(sent(up(x))) → CHECK(rec(x))
CHECK(rec(x)) → CHECK(x)
REC(up(x)) → REC(x)
TOP(no(up(x))) → REC(x)
TOP(sent(up(x))) → TOP(check(rec(x)))
REC(no(x)) → SENT(rec(x))
CHECK(sent(x)) → SENT(check(x))
CHECK(rec(x)) → REC(check(x))
TOP(no(up(x))) → CHECK(rec(x))
CHECK(no(x)) → NO(check(x))
REC(sent(x)) → SENT(rec(x))
CHECK(up(x)) → CHECK(x)
TOP(sent(up(x))) → REC(x)
TOP(rec(up(x))) → CHECK(rec(x))
TOP(no(up(x))) → TOP(check(rec(x)))
REC(no(x)) → REC(x)
NO(up(x)) → NO(x)
SENT(up(x)) → SENT(x)
TOP(rec(up(x))) → TOP(check(rec(x)))
REC(sent(x)) → REC(x)
CHECK(sent(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

CHECK(no(x)) → CHECK(x)
TOP(rec(up(x))) → REC(x)
REC(bot) → SENT(bot)
REC(rec(x)) → SENT(rec(x))
CHECK(rec(x)) → CHECK(x)
TOP(sent(up(x))) → CHECK(rec(x))
REC(up(x)) → REC(x)
TOP(no(up(x))) → REC(x)
TOP(sent(up(x))) → TOP(check(rec(x)))
REC(no(x)) → SENT(rec(x))
CHECK(sent(x)) → SENT(check(x))
CHECK(rec(x)) → REC(check(x))
TOP(no(up(x))) → CHECK(rec(x))
CHECK(no(x)) → NO(check(x))
REC(sent(x)) → SENT(rec(x))
CHECK(up(x)) → CHECK(x)
TOP(sent(up(x))) → REC(x)
TOP(rec(up(x))) → CHECK(rec(x))
TOP(no(up(x))) → TOP(check(rec(x)))
REC(no(x)) → REC(x)
SENT(up(x)) → SENT(x)
NO(up(x)) → NO(x)
TOP(rec(up(x))) → TOP(check(rec(x)))
REC(sent(x)) → REC(x)
CHECK(sent(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 5 SCCs with 13 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

NO(up(x)) → NO(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

NO(up(x)) → NO(x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
NO(x1) = NO(x1)
up(x1) = up(x1)

Lexicographic path order with status [19].
Precedence:

up₁ > NO₁

Status:

NO₁: [1]
up₁: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SENT(up(x)) → SENT(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SENT(up(x)) → SENT(x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SENT(x1) = SENT(x1)
up(x1) = up(x1)

Lexicographic path order with status [19].
Precedence:

up₁ > SENT₁

Status:

up₁: multiset
SENT₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REC(up(x)) → REC(x)
REC(no(x)) → REC(x)
REC(sent(x)) → REC(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REC(sent(x)) → REC(x)

The remaining pairs can at least be oriented weakly.

REC(up(x)) → REC(x)
REC(no(x)) → REC(x)

Used ordering: Combined order from the following AFS and order.
REC(x1) = REC(x1)
up(x1) = x1
no(x1) = x1
sent(x1) = sent(x1)

Lexicographic path order with status [19].
Precedence:

trivial

Status:

REC₁: [1]
sent₁: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REC(up(x)) → REC(x)
REC(no(x)) → REC(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REC(up(x)) → REC(x)

The remaining pairs can at least be oriented weakly.

REC(no(x)) → REC(x)

Used ordering: Combined order from the following AFS and order.
REC(x1) = REC(x1)
up(x1) = up(x1)
no(x1) = x1

Lexicographic path order with status [19].
Precedence:

up₁ > REC₁

Status:

up₁: multiset
REC₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REC(no(x)) → REC(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REC(no(x)) → REC(x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
REC(x1) = REC(x1)
no(x1) = no(x1)

Lexicographic path order with status [19].
Precedence:

no₁ > REC₁

Status:

no₁: multiset
REC₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

              ↳ QDP

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CHECK(no(x)) → CHECK(x)
CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → CHECK(x)
CHECK(rec(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

CHECK(no(x)) → CHECK(x)

The remaining pairs can at least be oriented weakly.

CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → CHECK(x)
CHECK(rec(x)) → CHECK(x)

Used ordering: Combined order from the following AFS and order.
CHECK(x1) = CHECK(x1)
no(x1) = no(x1)
up(x1) = x1
sent(x1) = x1
rec(x1) = x1

Lexicographic path order with status [19].
Precedence:

no₁ > CHECK₁

Status:

no₁: multiset
CHECK₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → CHECK(x)
CHECK(rec(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

CHECK(rec(x)) → CHECK(x)

The remaining pairs can at least be oriented weakly.

CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → CHECK(x)

Used ordering: Combined order from the following AFS and order.
CHECK(x1) = CHECK(x1)
up(x1) = x1
sent(x1) = x1
rec(x1) = rec(x1)

Lexicographic path order with status [19].
Precedence:

trivial

Status:

rec₁: multiset
CHECK₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

CHECK(up(x)) → CHECK(x)

The remaining pairs can at least be oriented weakly.

CHECK(sent(x)) → CHECK(x)

Used ordering: Combined order from the following AFS and order.
CHECK(x1) = CHECK(x1)
up(x1) = up(x1)
sent(x1) = x1

Lexicographic path order with status [19].
Precedence:

up₁ > CHECK₁

Status:

up₁: multiset
CHECK₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CHECK(sent(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

CHECK(sent(x)) → CHECK(x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
CHECK(x1) = CHECK(x1)
sent(x1) = sent(x1)

Lexicographic path order with status [19].
Precedence:

sent₁ > CHECK₁

Status:

CHECK₁: [1]
sent₁: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ PisEmptyProof

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(no(up(x))) → TOP(check(rec(x)))
TOP(sent(up(x))) → TOP(check(rec(x)))
TOP(rec(up(x))) → TOP(check(rec(x)))

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TOP(no(up(x))) → TOP(check(rec(x)))

The remaining pairs can at least be oriented weakly.

TOP(sent(up(x))) → TOP(check(rec(x)))
TOP(rec(up(x))) → TOP(check(rec(x)))

Used ordering: Combined order from the following AFS and order.
TOP(x1) = TOP(x1)
no(x1) = no(x1)
up(x1) = x1
check(x1) = x1
rec(x1) = x1
sent(x1) = x1
bot = bot

Lexicographic path order with status [19].
Precedence:

no₁ > TOP₁

Status:

no₁: [1]
bot: multiset
TOP₁: [1]

The following usable rules [14] were oriented:

rec(sent(x)) → sent(rec(x))
no(up(x)) → up(no(x))
check(no(x)) → no(x)
check(up(x)) → up(check(x))
rec(up(x)) → up(rec(x))
check(rec(x)) → rec(check(x))
rec(no(x)) → sent(rec(x))
check(sent(x)) → sent(check(x))
check(no(x)) → no(check(x))
sent(up(x)) → up(sent(x))
rec(bot) → up(sent(bot))
rec(rec(x)) → sent(rec(x))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TOP(sent(up(x))) → TOP(check(rec(x)))
TOP(rec(up(x))) → TOP(check(rec(x)))

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.